The typical design methodology for integrated circuit designs—such as very large scale integrated (VLSI) circuits and application specific integrated circuits (ASICs)—is conventionally divided into the following three stages. First, a design capture step is performed using, for example, a high-level language synthesis package. Next, design verification is made on the resulting design. This includes simulations, timing analysis, and automatic test pattern generation (ATPG) tools. Finally, there is layout and eventual tape out of the device. The device is then tested, and the process may need to be reiterated one or more times until the desired design criteria are satisfied.
The design capture step typically involves the specification of a logic circuit by a designer. A hardware description language (“HDL”) provides the designer with a mechanism for describing the operation of the desired logic circuit in a technology-independent manner.
Automated software tools available from companies such as Cadence Design Systems and Synopsys take an HDL description of the integrated circuit (sometimes referred to as a behavioral or register-transfer-level description) and map it into an equivalent netlist composed of the standard cells from a selected standard cell library. This process is commonly known as “synthesis.”
A netlist is a data structure representation of the electronic logic system that comprises a set of modules, each of which comprises a data structure that specifies sub-components and their interconnection. The netlist describes the way standard cells and blocks are interconnected. Netlists are typically available in Verilog, EDIF (Electronic Design Interchange Format), or VHDL (Very High Speed Integrated Circuit Hardware Design Language) formats. Other software tools available from companies such as Cadence or Synopsys take a netlist comprised of standard cells and create a physical layout of the chip by placing the cells relative to each other to minimize timing delays or wire lengths, and then create electrical connections (or routing) between the cells to physically complete the desired circuit. Once a netlist has been generated from the logic design, silicon compilers, also called place and route tools, convert the netlist into a semiconductor circuit layout. The semiconductor circuit layout specifies the physical implementation of the circuit in silicon or other semiconductor materials.
Design verification involves verifying that the logic definition is correct, that the circuit implements the function expected by the designers, and that the many optimizations and transformations introduced during the design process do not alter the intended logical function of the design. Design verification may involve timing analysis and simulation tools. The data representation in the logic design database may be reformatted as needed prior to use by the timing analysis and simulation tools. The design undergoes design verification analysis in order to detect flaws in the design. The design is also analyzed using simulation tools to assess the functionality of the design. If errors are found or the resulting functionality is unacceptable, the designer modifies the design as needed. These design iterations help to ensure that the design satisfies its requirements.
Other verification methods include generating large numbers of test programs, either manually or with the help of various random and specific test generators, and running those test programs on a simulator that models the device operation. Formal verification (property checking) may also be used to prove correct behavior for selected aspects of the design. Formal verification is a technique that models a logic circuit as a state transition system using specifications for components in the system. For performance and productivity reasons, the simulations and formal checks are typically applied at the highest level (most abstract) model available, often a high level description of the design written in register transfer level VHDL or Verilog.
Historically, gate-level simulation on the final implementation netlist was used to check for functional errors that may have been introduced during the optimization and transformation process. Two models can theoretically be proven equivalent by exhaustive simulation. However, to achieve complete coverage by simulation, the results of 2(n+m) simulation stimuli need to be checked, where n and m represent the number of circuit inputs and registers, respectively. Given the large number of circuit inputs and registers, this approach is not feasible, even for small designs. Practically, one would compromise the verification coverage by simulating only a small fraction of the possible simulation patterns.
Equivalence-checking is a formal verification technique used to check that two representations (or models) of an integrated circuit design are functionally equivalent. In an embodiment, special data structures and techniques such as Binary Decision Diagrams (BDD) and propositional satisfiability (SAT) are used to symbolically represent the state transitions of the designs and implicitly enumerate all possible stimuli. The two models to be compared can be at the same or on quite different levels of abstraction. For example, the first model could be represented at the register-transfer-level (for example, VHDL or Verilog) as a high-level design view defining the desired system functionality. The second model might be a gate or transistor-level representation of the actual circuit implementation. A proof of model equivalence implicitly validates any results from functional simulation computed on either model for both models. In a typical case, the high-level design view is extensively simulated to check the intended function of a system. Successful equivalence checks of the high-level view with the low-level implementation automatically extend the validity of the system simulation to the implementation.
Equivalence-checking tools commonly used in industry generally perform “combinational equivalence checking,” which means they actually compare only the combinational logic between matched primary inputs, primary outputs, and internal memory elements (registers). Each primary output and internal register is treated as a comparison point that terminates a cone of combinational logic, and each internal register and primary input are treated as an input point that sources the cones of logic feeding one or more comparison points. First, a correspondence is established that maps all comparison points and input points in the reference design (model 1) to comparison points and input points in the revised design (model 2), and the logic function of each comparison point is extracted so that they may be compared for functional equivalence. If such a correspondence can be established for all comparison points, and if the formal analysis proves that all comparison points are functionally equivalent for all possible assignments of binary values to the input points, then it follows that the two models are functionally equivalent. Equivalence checking tools are commonly used to ensure that each new revision of a design remains functionally equivalent to the original high-level description.
It should be noted that although combinational equivalence-checking can definitively prove that two models are functionally equivalent, it cannot definitively prove non-equivalence due to the automatic treatment of internal registers as both comparison points and input points, which was done to reduce the sequential equivalency checking problem into a combinational one. It is quite possible for the equivalence check to report a difference in the combinational function at a comparison point that does not actually result in a difference in the sequential behavior as observed at the primary outputs of the design. Inserting cut-points to partition the designs at the internal registers introduces independent variables that can potentially result in “false negatives.” In practice, however, the types of transformations made during a design process typically do not alter the combinational function of internal registers, so the tools are widely applicable.
One common situation where equivalence checking will report false-negatives is when one model is missing function that is present in the other model. For example, the design process may include a step that automatically inserts scan structures for manufacturing tests. In such cases, since the revised model has the additional test logic function which the original model does not, it is necessary to constrain the equivalence check such that the functional differences are masked, for example by asserting one or more signals (usually primary inputs) to values that disable the test logic function. Although the test logic that was inserted is not verified, the remaining logic is.
Another situation where false-negatives can and do arise is when scan chain connections between registers are reordered, which may be done to minimize overall wire length in a design based on new placement information. Since the scan connection and the associated test logic are part of the combinational logic cone of the comparison points resulting from internal registers, any changes to those connections will change the function of the combinational logic. In general, however, the exact order of the scan chain connections is relevant only to the ATPG (automatic test pattern generation) tools that must create the patterns for manufacturing test—the order does not affect the non-test function of the design. One solution, then, is to constrain the equivalence check, as previously described above, such that differences due to the test logic function are masked, for example by asserting scan clocks or scan enable signals to inactive values. The remaining logic function not directly associated with the test logic function is then verified.
This solution can leave a significant exposure for some design processes employing an LSSD (level sensitive scan design) style. In LSSD, registers are implemented as pairs of latches, usually called L1 and L2, which have three distinct clocks, usually called A, B and C. The A and C clocks are the enables of the L1 latch, which is dual ported. The A clock loads the scan data input and the C clock loads the functional data input. The B clock is the enable for the L2 latch and loads the data that is the output from the L1 latch. During normal (functional) operation, the A clock is held inactive, and the C and B clocks are pulsed in a non-overlapping manner to give the desired function of a register. During scan operation, however, the C clock is held inactive, and the A and B clocks are pulsed in a non-overlapping manner to scan the desired test pattern sequence through the LSSD registers in the scan chain.
It is also possible to assert both the A and B clocks active simultaneously while the C clock is held inactive, which enables both the L1 and L2 latches in the LSSD register to “flush” the scan in value immediately to the output. In such a situation, the LSSD register is acting like a combinational buffer, allowing a value at the primary scan input of the design to propagate through the entire scan chain. This feature of LSSD-based scan chains is often used to initialize the internal registers of the design to their reset state during power-on reset of the hardware. For example, if the primary scan input is asserted to logic 0 during the LSSD flush operation, that logic 0 will propagate to all LSSD registers in the scan chain to effectively reset them all to zero. If a particular LSSD register needs to be reset to a logic 1 instead, inverters can be inserted into the scan chain before and after that register to achieve the desired logic 1 value during flush operation.
When scan logic does not exist in the original model, but has been inserted into the revised model either manually or by an automated test-logic insertion process, the desired reset state values for the registers are typically specified either in a separate file or as initial value attributes in the HDL for the original model. As the test-logic insertion process converts flip-flops into LSSD registers and connects them into one or more scan chains, it must also add inverters or other logic as needed to produce the desired reset state during a flush scan operation. The previously discussed approach of constraining the equivalence check to mask out the test logic function will not guarantee that the revised model exhibits the desired reset state under flush scan operation.
Similarly, reordering the scan chains in a process where LSSD flush operation is used to set the power-on reset state is still possible, but care must be taken to ensure that the effective reset state is not altered. Since a proper power-on reset condition is critical to proper operation of the hardware, it is imperative that the reset values are validated. The previously discussed approach of constraining the equivalence check to mask out the scan logic will obviously not guarantee that the reset values remain consistent.
Thus, without a better way to handle scan chains, combinational equivalence checking cannot be used to validate the flush reset state, requiring the development of an otherwise unnecessary simulation environment for flush reset verification, which increases the cost and the development time of integrated circuits.